the_es:ES, e':E, l:IdLnk, m:Msg.
(m  snds(l;before(e')))  (e:E. ((e <loc e') & (m  sends(l;e)))) 

latex

Definitions	x:A. B(x), P  Q, snds(l;before(e)), x:A. B(x), P & Q, P  Q, , P  Q, t  T, S  T, x. t(x), A c B, (Msg on l), x(s)
Lemmas	iff functionality wrt iff, l member wf, concat wf, map wf, es-sends wf, es-Msgl wf, es-before wf, es-locl wf, member-concat, exists functionality wrt iff, and functionality wrt iff, member map, member-es-before, es-Msg wf, IdLnk wf, es-E wf, event system wf